$\forall$${\it the\_w}$:World, ${\it tg}$:Id, ${\it mss}$:(Msg List). w{-}tagged(${\it tg}$;${\it mss}$) $\in$ (Msg List)